finite{-}prob{-}space
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{$p$:rationals List$\mid$ (qsum(0; $\parallel$$p$$\parallel$; $i$.$p$[$i$]) = 1) $\wedge$ l\_all($p$; rationals; $q$.qle(0; $q$))\}